\begin{figure}[H]
\centering
\begin{subfigure}[b]{.4\textwidth}
\centering
\figscale{
\begin{tikzpicture}[%
    >=stealth,
    shorten >=1pt,
    node distance=2cm,
    on grid,
    auto,
    state/.append style={minimum size=2em},
    thick,
    scale=0.4
  ]
    \node[state, rectangle, align=center] (N1) {$A$\\$\textcolor{BrickRed}{(\textcolor{Blue}{EX(\textcolor{OliveGreen}{\$B})} \rightarrow \textcolor{BurntOrange}{EX(\textcolor{Sepia}{\$C})})}$};
    \node[state] (N2) at (-4, -4) {$B$};
    \node[state] (N3) at (4, -4) {$C$};
\node[state] (N4) at (0, -8) {$D$};

    \path[->, BrickRed]
              (N1) edge [loop above] node {$\textcolor{Plum}{AX(\textcolor{OrangeRed}{!\textcolor{ProcessBlue}{\$D}})}\textcolor{Black}{, }\textcolor{BurntOrange}{EX(\textcolor{Sepia}{\$C})}$} (N1);

\path[->, Plum]
              (N1) edge node [above left, pos=0.75] {$\textcolor{OrangeRed}{!\textcolor{ProcessBlue}{\$D}}$} (N2)
              (N1) edge [bend right] node [below left] {$\textcolor{OrangeRed}{!\textcolor{ProcessBlue}{\$D}}$} (N3);

\path[->, BurntOrange]
              (N1) edge node [above right, pos=0.75] {$\textcolor{Sepia}{\$C}$} (N3);

\path[->]
	(N2) edge node {} (N4)
	(N3) edge node {} (N4);
  \end{tikzpicture}
}
\caption{Affichage \texttt{.dot}}
\end{subfigure}
\begin{subfigure}[b]{.4\textwidth}
\centering
\begin{minipage}{0.7\linewidth}
\begin{verbatim}
(EX($D) -> EX($C)) = { 0 }
  AX(!$D) = { 0 }
    !$D = { 1 3 }
      $D = { 2 }
  EX($C) = { 0 }
    $C = { 3 }
\end{verbatim}
\end{minipage}
\caption{Affichage textuel}
\end{subfigure}
\caption{Preuve de $EX(\$D)\rightarrow EX(\$C)$ pour l'état 0}
\label{fig:PreuveOperateurImply2}
\end{figure}